$\forall$${\it es}$:ES, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $P$:(E$\rightarrow\mathbb{P}$).
\\[0ex]$R$ =$>$ $\lambda$$e$,${\it e'}$. ($e$ $<$ ${\it e'}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:E. ($P$($x$) \& $P$($y$)) $\Rightarrow$ ((($R$($x$,$y$)) $\vee$ ($x$ = $y$)) $\vee$ ($R$($y$,$x$))))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:E. ($P$($x$) \& $P$($y$)) $\Rightarrow$ (($R$($x$,$y$)) $\Leftarrow\!\Rightarrow$ ($x$ $<$ $y$)))